Include definedness checks during exhale#457
Conversation
This will allow one to be able to be able to do permission definendess checks in a different state than the standard evaluation state.
…permission checks The setDefState field in DefinednessState is now mutable such that when unfolding one can change the definedness state (assuming there is a separate definedness state). An alternative would be to keep the same definedness state during an unfolding statement but to then explicitly reset this state via a Boogie statement at the end of an unfolding. Since Boogie performs constant propagation the resulting VC should essentially be the same for both approaches. The currently implemented approach is more in-line with the way encoding is currently handled, where new states are constructed instead of reusing previous states.
…nedness check) o special treatment for permission introspection since permission introspection within unfoldings still needs to be explored properly
…inside a package statement
…nedness state. As a result, we can remove the predicate in this state (but do not check whether it is there, because in this mode well-definedness is assumed; analogous to inhale).
… exhale this check should not be required, but I add it as a sanity check
…state if the exhale is non-empty
|
One aspect that this PR does not resolve and that should be handled in another PR is when one of the following two cases occur during an exhale:
The expected behavior is to evaluate those occurrences of permission introspection in the evaluation permission mask, that is, the mask which the exhale modifies when permissions are removed. Currently, these occurrences are evaluated in the well-definedness permission mask, that is, the permission mask right before the exhale. The code contains |
Update tests for Carbon exhale with well-definedness change (Carbon PR viperproject/carbon#457)
1 participant
Previously, the encoding for
exhale Afirst checked well-definedness ofAand in a second step performed the actual exhale. This approach is flawed, because (1) well-definedness ofAdepends on the actual exhale in the general case and (2) in cases where the exhale fails, the reported errors are not the expected ones. See #406 for examples illustrating these two problems.This PR implements an exhale implementation, which (if enabled) does the well-definedness checks during the exhale (as we already do with inhale).